@i k(v:T) triggers local action a
@i when P (x:A) v
== (vartype(i;x) r A) & e@i. (kind(e) = k)  (valtype(e) r T)
== & e'@i. (kind(e') = locl(a))  (e:E. ((e <loc e') & kind(e) = k & ((P((x when e),val(e))))))
== & e@i. (kind(e) = k)  ((P((x when e),val(e))))  e'@i.kind(e') = locl(a) 

latex

---

clarification:

trigger1-p(es;T;A;P;i;k;a;x)
== (es-vartype(es; i; x) r A)
== & alle-at(es;i;e.(es-kind(es; e) = k  Knd)  (es-valtype(es; e) r T))
== & alle-at(es;i;e'.(es-kind(es; e') = locl(a)  Knd)
== &  (e:es-E(es)
== &  ((es-locl(es; e; e')
== &  (& es-kind(es; e) = k  Knd
== &  (& ((P(es-when(es; x; e),es-val(es; e)))))))
== & alle-at(es;i;e.(es-kind(es; e) = k  Knd)
== &  ((P(es-when(es; x; e),es-val(es; e))))
== &  existse-at(es; i; e'.(es-kind(es; e') = locl(a)  Knd))) 

latex

Definitions	vartype(i;x), valtype(e), x:A. B(x), E, (e <loc e'), P & Q, e@i. P(e), P  Q, b, f(a), x when e, val(e), e@i.P(e), s = t, Knd, kind(e), locl(a)
FDL editor aliases	trigger1-p